/*
 * Atomic Predicates for Transformers
 * 
 * Copyright (c) 2015 UNIVERSITY OF TEXAS AUSTIN. All rights reserved. Developed
 * by: HONGKUN YANG and SIMON S. LAM http://www.cs.utexas.edu/users/lam/NRL/
 * 
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * with the Software without restriction, including without limitation the
 * rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
 * sell copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 * 
 * 1. Redistributions of source code must retain the above copyright notice,
 * this list of conditions and the following disclaimers.
 * 
 * 2. Redistributions in binary form must reproduce the above copyright notice,
 * this list of conditions and the following disclaimers in the documentation
 * and/or other materials provided with the distribution.
 * 
 * 3. Neither the name of the UNIVERSITY OF TEXAS AUSTIN nor the names of the
 * developers may be used to endorse or promote products derived from this
 * Software without specific prior written permission.
 * 
 * 4. Any report or paper describing results derived from using any part of this
 * Software must cite the following publication of the developers: Hongkun Yang
 * and Simon S. Lam, Scalable Verification of Networks With Packet Transformers
 * Using Atomic Predicates, IEEE/ACM Transactions on Networking, October 2017,
 * Volume 25, No. 5, pages 2900-2915 (first published as IEEE Early Access
 * Article, July 2017, Digital Object Identifier: 10.1109/TNET.2017.2720172).
 * 
 * 
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * CONTRIBUTORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS WITH
 * THE SOFTWARE.
 */
package transformer;

import java.util.*;

import common.*;
import jdd.bdd.BDD;


public class DeviceStanford extends Device {

      /**
     * 
     */
    private static final long serialVersionUID = 5536987024539747299L;
    HashMap<String, LinkedList<ACLRule>> aclmap;
      HashMap<String, Integer> rawacl;
      HashSet<Integer> rawaclinuse;
      // subnet name -> subnet info
      HashMap <String, ArrayList<Subnet>> subnets;
      HashMap<String, HashSet<String>> vlan_ports;
      ArrayList<ACLUse> acluses;
      // portname -> acl bdd, should be physical port
      // combined with vlan info
      HashMap<String, Integer> inaclbdds;
      HashMap<String, Integer> outaclbdds;
      HashMap<String, FWDAPSet> inaclaps;
      HashMap<String, FWDAPSet> outaclaps;
      
      public void setaps(APComputer apc) {

          super.setaps(apc);
          //inaclaps = new HashMap<String, FWDAPSet>();
          //outaclaps = new HashMap<String, FWDAPSet>();
          //setaps_1(inaclaps, inaclbdds, apc);
          //setaps_1(outaclaps, outaclbdds, apc);

          
      }
      
     
      
      public PositionTuple add_nat()
      {
            String port = "nat_port" + nat_subnet_id;
            nat_subnet_id ++;
            int nat_addr_bdd = baw.encodeDstIPPrefix(nat_addr, 32);
            nat_addr ++;
            
            fwbdds.put(port, nat_addr_bdd);
            return new PositionTuple(name, port);
      }
      
      public DeviceStanford(String dname)
      {
            super(dname);
            aclmap = new HashMap<String, LinkedList<ACLRule>>();
            fws = new ArrayList<ForwardingRule>();
            vlan_ports = new HashMap<String, HashSet<String>>();
            acluses = new ArrayList<ACLUse>();
            subnets = new HashMap<String, ArrayList<Subnet>> ();
      }
      
      public void computeRawACL()
      {
            rawacl = new HashMap<String, Integer> ();
            for(String aclname : aclmap.keySet())
            {
                  rawacl.put(aclname, baw.ConvertACLs(aclmap.get(aclname)));
            }
            
            //System.out.println(rawacl);
      }

      public void computeACLBDDs()
      {
            computeRawACL();
            rawaclinuse = new HashSet<Integer>();
            HashMap<String, ArrayList<Integer>> inaclbddset = new HashMap<String, ArrayList<Integer>> ();
            HashMap<String, ArrayList<Integer>> outaclbddset = new HashMap<String, ArrayList<Integer>> ();
            for(int i = 0; i < acluses.size(); i ++)
            {
                  ACLUse oneacluse = acluses.get(i);
                  ArrayList<Subnet> subs = subnets.get(oneacluse.getinterface());
                  //System.out.println(oneacluse);
                  int rawaclbdd;
                  if(rawacl.containsKey(oneacluse.getnumber()))
                  {

                        rawaclbdd = rawacl.get(oneacluse.getnumber());
                        rawaclinuse.add(rawaclbdd);
                  }else
                  {
                        // cannot find the acl
                        continue;
                  }
                  HashSet<String> ports;
                  if(vlan_ports.containsKey(oneacluse.getinterface()))
                  {
                        ports = vlan_ports.get(oneacluse.getinterface());
                  }else
                  {
                        ports = new HashSet<String> ();
                        ports.add(oneacluse.getinterface());
                  }
                  if(oneacluse.isin())
                  {
                        int aclbdd = baw.encodeACLin(subs, rawaclbdd, ports.size());
                        //System.out.println(oneacluse);

                        for(String pport : ports)
                        {
                              if(inaclbddset.containsKey(pport))
                              {
                                    inaclbddset.get(pport).add(aclbdd);
                              }else
                              {
                                    ArrayList<Integer> newset = new ArrayList<Integer>();
                                    newset.add(aclbdd);
                                    inaclbddset.put(pport, newset);
                              }
                        }
                  }else
                  {
                        int aclbdd = baw.encodeACLout(subs, rawaclbdd, ports.size());
                        for(String pport : ports)
                        {
                              if(outaclbddset.containsKey(pport))
                              {
                                    outaclbddset.get(pport).add(aclbdd);
                              }else
                              {
                                    ArrayList<Integer> newset = new ArrayList<Integer>();
                                    newset.add(aclbdd);
                                    outaclbddset.put(pport, newset);
                              }
                        }
                  }
            }

            inaclbdds = new HashMap<String, Integer>();
            outaclbdds = new HashMap<String, Integer>();
            for(String pport : inaclbddset.keySet())
            {
                  ArrayList<Integer> bddset = inaclbddset.get(pport);
                  int [] bdds = Utility.ArrayListToArray(bddset);
                  //System.out.println(bdds.length);
                  int andbdd = baw.AndInBatch(bdds);
                  baw.DerefInBatch(bdds);
                  inaclbdds.put(pport, andbdd);
            }
            for(String pport : outaclbddset.keySet())
            {
                  ArrayList<Integer> bddset = outaclbddset.get(pport);
                  int [] bdds = Utility.ArrayListToArray(bddset);
                  int andbdd = baw.AndInBatch(bdds);
                  baw.DerefInBatch(bdds);
                  outaclbdds.put(pport, andbdd);
            }

            //System.out.println("in: " + inaclbdds);
            //System.out.println("out: " + outaclbdds);
      }


      public HashSet<String> vlanToPhy(String vlanport)
      {
            return vlan_ports.get(vlanport);
      }

      
      @Override
      public HashMap<String, Integer> ForwardAction(String port, int apt) {
HashMap <String, Integer> fwded = new HashMap<String, Integer>();
            
            BDD thebdd = baw.getBDD();

            // in acl
            int aptmp = apt;
            thebdd.ref(aptmp);
            
            if(inaclbdds.containsKey(port))
            {
                  aptmp = thebdd.andTo(aptmp, inaclbdds.get(port));
            }

            //System.out.println(fwaps.keySet());

            Iterator iter = fwbdds.entrySet().iterator();
            while(iter.hasNext())
            //for(String otherport : fwaps.keySet())
            {
                  Map.Entry entry = (Map.Entry) iter.next();
                  String otherport = (String) entry.getKey();
                  //
                  if(!otherport.equals(port))
                  {
                        int aptmp1 = thebdd.ref(thebdd.and(aptmp, (Integer)entry.getValue()));
                  
                        
                        if(aptmp1 != BDDACLWrapper.BDDFalse)
                        {
                              /*
                               * map vlan to physical port
                               */
                              if(otherport.startsWith("vlan"))
                              {
                                    HashSet<String> phyports = vlanToPhy(otherport);
                                    if(phyports == null)
                                    {

                                    }else
                                    {
                                          for(String pport:phyports)
                                          {
                                                // cannot go back to the incoming port
                                                if(!pport.equals(port))
                                                {
                                                      // out acl
                                                      int aptmp2 = thebdd.ref(aptmp1);
                                                      if(outaclbdds.containsKey(pport))
                                                      {
                                                            aptmp2 = thebdd.andTo(aptmp2, outaclbdds.get(pport));
                                                      }
                                                      if(aptmp2 != BDDACLWrapper.BDDFalse)
                                                      {
                                                            fwded.put(pport, aptmp2);
                                                      }
                                                }
                                          }
                                    }
                              }else{
                                    // out acl
                                    if(outaclbdds.containsKey(otherport))
                                    {
                                          aptmp1 = thebdd.andTo(aptmp1, outaclbdds.get(otherport));
                                    }
                                    if(aptmp1 != BDDACLWrapper.BDDFalse)
                                    {
                                          fwded.put(otherport, aptmp1);
                                    }
                              }
                        }
                  }
            }

            return fwded;
      }
      
      /**
       * 
       
      public HashMap <String, FWDAPSet> ForwardAction(String port, FWDAPSet fwdaps)
      {
          HashMap <String, FWDAPSet> fwded = new HashMap<String, FWDAPSet>();

          // in acl
          FWDAPSet fwtmp = new FWDAPSet(fwdaps);
          
          if(inaclaps.containsKey(port))
          {
              fwtmp.intersect(inaclaps.get(port));
          }

          //System.out.println(fwaps.keySet());

          //Iterator iter = fwaps.entrySet().iterator();
          //while(iter.hasNext())
          for(String otherport : fwaps.keySet())
          {
              //Map.Entry entry = (Map.Entry) iter.next();
              //String otherport = (String) entry.getKey();
              //
              if(!otherport.equals(port))
              {
                  FWDAPSet fwtmp1 = new FWDAPSet(fwtmp);
                  //fwtmp1.intersect((FWDAPSet) entry.getValue());
                  fwtmp1.intersect(fwaps.get(otherport));
                  
                  if(!fwtmp1.isempty())
                  {
                      
                       // map vlan to physical port
                      
                      if(otherport.startsWith("vlan"))
                      {
                          HashSet<String> phyports = vlanToPhy(otherport);
                          if(phyports == null)
                          {

                          }else
                          {
                              for(String pport:phyports)
                              {
                                  FWDAPSet fwtmp2 = new FWDAPSet(fwtmp1);
                                  // cannot go back to the incoming port
                                  if(!pport.equals(port))
                                  {
                                      // out acl
                                      
                                      if(outaclaps.containsKey(pport))
                                      {
                                          fwtmp2.intersect(outaclaps.get(pport));
                                      }
                                      if(!fwtmp2.isempty())
                                      {
                                          fwded.put(pport, fwtmp2);
                                      }
                                  }
                              }
                          }
                      }else{
                          // out acl
                          
                          if(outaclaps.containsKey(otherport))
                          {
                              fwtmp1.intersect(outaclaps.get(otherport));
                          }
                          if(!fwtmp1.isempty())
                          {
                              fwded.put(otherport, fwtmp1);
                          }
                      }
                  }
              }
          }

          return fwded;
      }
      **/

      
      public void computeFWBDDs()
      {
            Collections.sort(fws);
            this.fwbdds = baw.getfwdbdds_sorted_no_store(fws);
            
            //this.fwbdds = DeviceAPT.baw.getfwdbdds(fws);
            //System.out.println(fwbdds.size());
            //for(String iname : fwbdds.keySet())
            //{
            //    System.out.println(iname + ": " + fwbdds.get(iname));
            //}
      }

      public void addACL(String name, LinkedList<ACLRule> acl)
      {
            aclmap.put(name, acl);
      }
      public void addFW(ForwardingRule fw)
      {
            fws.add(fw);
      }
      public void addVlanPorts(String vlan, HashSet<String> ports)
      {
            vlan_ports.put(vlan, ports);
      }
      public void addACLUse(ACLUse oneuse)
      {
            acluses.add(oneuse);
      }
      public void addSubnet(Subnet sub)
      {
            if(subnets.keySet().contains(sub.getname()))
            {
                  subnets.get(sub.getname()).add(sub);
            }else
            {
                  ArrayList<Subnet> subs = new ArrayList<Subnet>();
                  subs.add(sub);
                  subnets.put(sub.getname(), subs);
            }
      }

}
